The present invention relates to the field of computer-aided chip design and, in particular, to comparison of circuits performing finite precision arithmetic operations, for equivalence.
Improved information processing has led to an increase in the complexity of the chips being used. With an increase in the complexity, a larger number of semiconductor devices, like logic gates, memories, central processing units, etc, are integrated in a single chip. This has generated a further demand for improvement in the existing techniques for circuit verification. In the rest of this application ‘circuit’ and ‘chip’ will be used interchangeably.
The process of circuit verification begins with the designing of the desired circuit. Circuits are designed using known computer-aided design tools, like Gemini CSX available from IKOS Systems, Cupertino, Calif., and System Realizer available from Quickturn Design Systems, Mountain View, Calif. These computer aided design tools use higher-level programming languages and Register Transfer Level (RTL) hardware programming languages to design a circuit. The higher level programming languages, and the RTL languages that are commonly used for circuit design are C and C++, and Verilog and VHDL respectively.
There are two main approaches to verify the correctness of a circuit. The first approach is known as Model Checking. In this approach, abstract properties that a circuit should satisfy are defined first. These properties are commonly defined using temporal logic, such as Linear Temporal Logic (LTL). Once these properties are defined, the verification of the circuit proceeds by checking that all the models of the circuit satisfy the property.
The second approach is based on equivalence checking of a circuit against a ‘golden’ model, i.e., another circuit that has been previously verified to be correct. An equivalence check is used to verify that a given circuit is functionally equal to the golden model. The golden model can be a circuit designed by higher level programming languages, like C, C++, etc., or could be an earlier version of the RTL circuit that needs to be refined.
Two main techniques have evolved to test the equivalence of circuits. In the first approach, the circuits are simulated for all possible set of inputs and the respective outputs are tested for equivalence. This process typically proceeds by creating a simulation driver that produces the simulation inputs and a simulation monitor that monitors the simulation outputs for equivalence. A limitation attached to this method is that with an increase in the complexity of circuits, covering all possible sets of inputs for determining equivalence becomes difficult. In addition, for complex circuits the time taken for simulation becomes high and as a result, the process of circuit comparison becomes slow.
The second approach is based on testing the equivalence of circuits by formal verification methods. In this approach, typically a circuit and the corresponding golden model are synthesized into bit-level designs. These bit-level designs are typically compared, using either decision diagram based techniques or SAT-based techniques. In the decision diagram based techniques, the bit-level designs are converted into canonic representations, which are then compared for equality. The most commonly used canonic representations are the Binary Decision Diagrams (BDDs). The SAT-based techniques transform the bit-level designs into boolean clauses, so that the clauses are simultaneously satisfiable, if and only if the circuits are inequivalent. The satisfiability of the clauses is determined through search-based techniques.
The main drawback of both approaches is that they require synthesis of the circuits being compared into bit-level designs. The representation of the synthesis tends to be exponential if the circuits are complex. Consequently, these approaches become impractical for complex circuits.
The problem associated with the blowing up of bit-level synthesis of complex circuits has been overcome by word-level techniques. One of the components of the word-level techniques for checking circuit equivalence is the use of theorem-provers for proving equivalence of arithmetic expressions.
Theorem provers, such as Cooperating Validity Checker (CVC), CVC Lite, developed by the Formal Verification Group of Stanford University, and Integrated Canonizer and Solver (ICS) developed by SRI, can be used to prove the equivalence of arithmetic expressions. These techniques check the equivalence of circuits involving arithmetic operations such as addition, subtraction, multiplication, division and comparison operations, such as ‘less-than’, etc. These theorem proving techniques use the associativity of addition and multiplication, and the distributivity of multiplication over addition, to transform arithmetic expressions into a unique canonic form, which can be compared for equality.
However, the theorem proving techniques such as CVC, CVC Lite and ICS can only test for the equivalence of arithmetic expressions of infinite precision. These techniques are not directly applicable for the comparison of circuits, since circuits are inherently associated with a finite precision. The principles of associativity and distributivity cannot be applied in the case of finite precision. For example, in the case of an infinite precision arithmetic expression such as a*(b+c), the principle of distributivity can be applied to obtain the equivalent expression a*b+a*c. However, such principles cannot be applied in a circuit with three finite width inputs, a, b and c that perform the operation a*(b+c), if the bit width of the output of any operator is different from that of the other operator. As a result, techniques such as CVC, CVC Lite and ICS cannot be directly used for the comparison of circuits.
In light of the preceding discussion, there exists a need for a method that efficiently compares arithmetic circuits with finite precision for equality. There is also a need of a method for circuit comparison that does not synthesize the circuits down to the bit-level. There is also a need of a method for circuit comparison that is computationally less intensive than the existing methods.